Implementing Herbelin's fix for the "NonPar" bug

Hugo Herbelin proposed to modify directly the function
"check_correct_par" to simplify commit c12b430
(see the pullrequest's discussion).

Note that the constructor "LocalNonPar" has now three arguments (instead
of two). In LocalNonPar (n,i,l) n denotes the position among real
arguments (ie. ignoring letins), i is the rel index of the expecting argument
in the context of parameters and l is the index of the inductive.

0 files changed, 0 insertions, 0 deletions