[Práctico 6] Ejercicio 3.2 - Hint

[Práctico 6] Ejercicio 3.2 - Hint

de Julian Tricanico Gadea -
Número de respuestas: 2

Buenas,

Me fijé por ejemplo en esta página https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html, pero cuando escribo

Hint Constructors BEval.

coq me escribe

Adding and removing hints in the core database implicitly is deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
Se podrá pasar algún pique de cómo usar Hint? (Por ejemplo para el ejercicio 3.2.)
Saludos!

                        

    
    
    
                            
    
    
                                

                                        
                                

    
                            
                    

                

            

        

    
        

                

                    

                        
                
                        

                            

                                        

                                                
                                        

                                

                                        En respuesta a Julian Tricanico Gadea
                                        
Re: [Práctico 6] Ejercicio 3.2 - Hint

                                        

                                            de Carlos Luna - 
                        

                                

                            

                
                            

                                        

                                        

                
                                

                                    

                                        
Hola.
Cambiaron varias cosas en la última versión de Coq...
Poné: Hint Constructors BEval : core.
Luego auto intentará aplicar los constructores de BEval cuando el goal sea de la forma BEval(...).
POR OTRA PARTE, el módiuo Omega y la táctica omega están descontinuados. Usar el módulo Lia y la táctica lia, en lugar de las anteriores.
Saludos, Carlos