diff options
Diffstat (limited to 'proofs/evar_refiner.mli')
| -rw-r--r-- | proofs/evar_refiner.mli | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 28c79d11e..ff986f3e6 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Names open Term open Environ @@ -16,9 +15,8 @@ open Evd open Refiner open Pretyping open Rawterm -(*i*) -(* Refinement of existential variables. *) +(** Refinement of existential variables. *) val w_refine : evar * evar_info -> (var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map @@ -26,4 +24,4 @@ val w_refine : evar * evar_info -> val instantiate_pf_com : Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map -(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) +(** the instantiate tactic was moved to [tactics/evar_tactics.ml] *) |