diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 61bc1ae7c..57987ef41 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -59,7 +59,7 @@ exception InductiveWithSort exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive -let dl = dummy_loc +let dl = Loc.ghost (* Some pre declaration of constant we are going to use *) let bb = constr_of_global Coqlib.glob_bool |